{-
 This file is part of the Clafer to Alloy Translator (clafer2alloy).

 Copyright (C) 2010 Kacper Bak <http://gsd.uwaterloo.ca/kbak>

 clafer2alloy is free software: you can redistribute it and/or modify
 it under the terms of the GNU Lesser General Public License as published by
 the Free Software Foundation, either version 3 of the License, or
 (at your option) any later version.

 clafer2alloy is distributed in the hope that it will be useful,
 but WITHOUT ANY WARRANTY; without even the implied warranty of
 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 GNU Lesser General Public License for more details.

 You should have received a copy of the GNU Lesser General Public License
 along with clafer2alloy. (See files COPYING and COPYING.LESSER.)  If not,
 see <http://www.gnu.org/licenses/>.
-}
module Skelclafer2alloy where

import Absclafer2alloy
import AlloyCode
import Common
import Data.Maybe
import Data.Function

-- -----------------------------------------------------------------------------
-- starts file with a header, adds all declarations and writes constraints for
-- top-level declarations
transModule :: Module -> Result
transModule x = case x of
  Module declarations  -> header ++ concatMap (declarations >>=)
    [transDeclaration] --, mkTopLevelConstraints]


transDeclaration :: Declaration -> Result
transDeclaration x = case x of
  EnumDecl id enumids  -> error "desugared"
  AbsClaferDecl gcard ident super attr elements  -> concat
    [ "abstract "
    , mkClaferDef declaration rels constraints
--    , noAbs name
    , elements']
    where
    (name, declaration, rels, constraints, elements') =
       mkClafer [] GCardEmpty ident super attr elements
  ClaferDecl clafer  -> concat [transCard "" $ getCard clafer, " ", transClafer [] clafer]
  ConstDecl constraint  -> mkFact $ transConstraint constraint


mkTopLevelConstraints :: Declaration -> Result
mkTopLevelConstraints x = case x of
  ClaferDecl clafer  ->
    mkFact $ mkCard "" transCard (transIdent $ getClaferId clafer) $ getCard clafer
  _ -> []


mkCard pre f param card
  | card' == set || card' == ""    = ""
  | card' `elem` [one, lone, some] = card'' ++ " " ++ param
  | otherwise                      = card''
  where
  card'  = f param card
  card'' = pre ++ " " ++ card'


transConstraint :: Constraint -> Result
transConstraint x = case x of
  Constraint essential lexps  -> foldWith " " $ map transLExp lexps


transClafer :: [String] -> Clafer -> Result
transClafer predecesors x = case x of
  Clafer gcard ident super attr essential card elements  -> if isReference x
    then "" else concat
    [ -- "lone"
--      transCard (mkName "_" id $ transIdent ident : predecesors) card
     mkClaferDef declaration rels (hConst predecesors name : constraints)
--    , mkFact $ 
    , elements']
    where
    (name, declaration, rels, constraints, elements') =
      mkClafer predecesors gcard ident super attr elements

-- -----------------------------------------------------------------------------
-- generic function for generating clafer's code
mkClafer :: [String] -> GCard -> Ident -> Super -> Attr -> Elements ->
  (Result, Result, [Result], [Result], Result)
mkClafer predecessors gcard ident super attr elements  =
  ( name
  , claferDecl name predecessors (transSuper super)
  , prnt : aRel : rels
  , mkSubConst gcard hNames (mkSubRel hNames gcard super elements hNames) : aConst : constraints
  , concat $ transElements (transElement hNames) elements)
  where
    name                = transIdent ident
    hNames              = name : predecessors
    (aRel, aConst)      = transAttr attr
    (rels, constraints) = unzip $ transElements (declElement hNames) elements
    prnt                = if null predecessors then "" else "parent : one " ++ mkName "_" id predecessors


-- TODO: list ALL references
listElement :: [String] -> Element -> Maybe Result
listElement predecessors x = case x of
  Subclafer clafer  ->
    Just $ mkName "_" id $ (transIdent $ getClaferId clafer) : [] --predecessors
  _ -> Nothing


mkSubRel :: [String] -> GCard -> Super -> Elements -> [String] -> Result
mkSubRel predecessors gCard super elements hNames
  | null subc = ""
  | otherwise = concat [foldWith " + " subc]
  where
  subc = catMaybes $ transElements (listElement predecessors) elements

mkSubConst :: GCard -> [String] -> String -> Result
mkSubConst gCard hNames sc = mkCard "" {-letSubclafers-} transGCard {-subclafers-} ("(" ++ sc ++ ")") gCard


-- -----------------------------------------------------------------------------
-- code generation for clafers and constraints
transElements :: (Element -> a) -> Elements -> [a]
transElements f x = case x of
  ElementsEmpty  -> error "desugared"
  Elements elements  -> map f elements


declElement :: [String] -> Element -> (Result, Result)
declElement predecessors x = case x of
  Subclafer clafer  -> if card `elem` [one, lone, some, set]
    then (sDecl card, const) else (sDecl set, const ++ card)
    where
    name    = transIdent $ getClaferId clafer
    card    = transCard name $ getCard clafer
    sDecl c = concat [name, " : ", c, " ", relType]
    -- TODO: const always empty
    (relType, const) = if isReference clafer
      then (transSExp $ getSExpAttr clafer, "")
      else (mkName "_" id $ name : predecessors, "")
  ClaferUse name essential card elements -> error "desugared"
  Subconstraint constraint  -> ("", transConstraint constraint)
  

transElement :: [String] -> Element -> Result
transElement predecesors x = case x of
  Subclafer clafer  -> transClafer predecesors clafer
  ClaferUse name essential card elements -> error "desugared"
  Subconstraint constraint  -> ""


-- -----------------------------------------------------------------------------
-- simple code generation functions
transEssential :: Essential -> Result
transEssential x = case x of
  EssentialEmpty  -> error "not implemented"
  Essential  -> error "not implemented"


transSuper :: Super -> (Maybe Result, Result)
transSuper x = case x of
  SuperEmpty  -> error "desugared"
  Super name  -> transName name


transAttr :: Attr -> (Result, Result)
transAttr x = case x of
  AttrEmpty  -> ("", "")
  AttrSExp modids sexp  ->
    (attrField ++ " : one " ++ baseClafer, mkAttribute $ transSExp sexp)
  AttrSuper modids sexp -> ("", mkAttribute $ transSExp sexp)


transGCard :: String -> GCard -> Result
transGCard name x = case x of
  GCardEmpty  -> ""
  GCardXor  -> error "desugared"
  GCardOr   -> error "desugared"
  GCardMux  -> error "desugared"
  GCardInterval (GNCard m n)  -> transNCard name (NCard m n)


transCard :: String -> Card -> Result
transCard name x = case x of
  CardEmpty  -> error "desugared"
  CardLone  -> error "desugared"
  CardSome  -> error "desugared"
  CardAny  -> error "desugared"
  CardInterval ncard  -> transNCard name ncard


transNCard :: String -> NCard -> Result
transNCard name x = case x of
  NCard 1 (ExIntegerNum 1) -> one
  NCard 0 (ExIntegerNum 1) -> lone
  NCard 1 ExIntegerAst     -> some
  NCard 0 ExIntegerAst     -> set
  NCard n exinteger  ->
    s1 ++ (if null s1 || null s2 then "" else " and") ++ s2
    where
    s1 = if n == 0 then "" else (show n) `less` (count name)
    s2 = transExInteger name exinteger


transExInteger :: String -> ExInteger -> Result
transExInteger name x = case x of
  ExIntegerAst  -> ""
  ExIntegerNum n  -> " " ++ (count name) `less` (show n)


transSExp :: SExp -> Result
transSExp x = case x of
  SExpUnion sexp0 sexp -> transS sexp0 "+" sexp
  SExpIntersection sexp0 sexp  -> transS sexp0 "&" sexp
  SExpDomain sexp0 sexp  -> transS sexp0 "<:" sexp
  SExpRange sexp0 sexp  -> transS sexp0 ":>" sexp
  SExpJoin sexp0 sexp  -> transS sexp0 "." sexp
  SExpArrow sexp0 sexp  -> error "desugared"
  SExpRIdent ident _ -> transIdent ident
  where
  transS = transBinOp transSExp


transLExp :: LExp -> Result
transLExp x = case x of
  EIff lexp0 iff lexp  -> transL lexp0 (transIff iff) lexp
  EImplies lexp0 implies lexp  -> transL lexp0 (transImplies implies) lexp
  EImpliesElse lexp0 implies lexp1 lexp  -> concat 
    [transLExp (EImplies lexp0 implies lexp1), " else (", transLExp lexp, ")"]
  EOr lexp0 or lexp  -> transL lexp0 (transOr or) lexp
  EXor lexp0 xor lexp  -> "not (" ++ transLExp (EIff lexp0 Iff lexp) ++ ")"
  EAnd lexp0 and lexp  -> transL lexp0 (transAnd and) lexp
  ENeg neg lexp  -> transNeg neg ++ "("  ++ transLExp lexp ++ ")"
  ETerm term  -> transTerm term
  where
  transL = transBinOp transLExp


transIff :: Iff -> Result
transIff x = case x of
  Iff  -> " <=> "


transImplies :: Implies -> Result
transImplies x = case x of
  Implies  -> " => "


transAnd :: And -> Result
transAnd x = case x of
  And  -> " && "


transXor :: Xor -> Result
transXor x = case x of
  Xor  -> " xor "


transOr :: Or -> Result
transOr x = case x of
  Or  -> " or "


transNeg :: Neg -> Result
transNeg x = case x of
  Neg  -> "not "


transTerm :: Term -> Result
transTerm x = case x of
  TermCmpExp cmpexp  -> transCmpExp cmpexp
  TermSet sexp        -> error "desugared"
  TermQuantSet quant sexp -> transQuant quant ++ " "  ++ transSExp sexp
  TermQuantDeclExp decls lexp -> concat
    [foldWith "| " (map transDecl decls), " | ",  transLExp lexp]


transCmpExp :: CmpExp -> Result
transCmpExp x = case x of
  ELt exp0 exp  -> transCmp exp0 " < " exp
  EGt exp0 exp  -> transCmp exp0 " > " exp
  EEq exp0 exp  -> transCmp exp0 " = " exp
  EREq exp0 exp  -> transCmp exp0 " = " exp
  ELte exp0 exp  -> transCmp exp0 " =< " exp
  EGte exp0 exp  -> transCmp exp0 " >= " exp
  ENeq exp0 exp  -> transCmp exp0 " != " exp
  ERNeq exp0 exp  -> transCmp exp0 " != " exp
  EIn exp0 exp  -> transCmp exp0 " in " exp
  ENin exp0 exp  -> transCmp exp0 " not in " exp
  where
  transCmp = transBinOp transExp


transBinOp f x op y = ((concWith op) `on` (brArg f)) x y

brArg f arg = "(" ++ f arg ++ ")"


transExp :: Exp -> Result
transExp x = case x of
  ESetExp sexp  -> transSExp sexp
  ENumExp aexp -> transAExp aexp
  EStrExp strexp -> error "analyzed"


transQuant :: Quant -> Result
transQuant x = case x of
  QuantNo   -> no
  QuantLone -> lone
  QuantOne  -> one
  QuantSome -> some


transExQuant :: ExQuant -> Result
transExQuant x = case x of
  ExQuantAll -> "all"
  ExQuant quant -> transQuant quant


transDecl :: Decl -> Result
transDecl x = case x of
  Decl exquant disj locids sexp -> concat [transExQuant exquant, " ",
    transDisj disj, " ",
    foldWith ", " (map transLocId locids), " : ", transSExp sexp]


transDisj :: Disj -> Result
transDisj x = case x of
  DisjEmpty -> ""
  Disj -> disj


transLocId :: LocId -> Result
transLocId x = case x of
   LocIdIdent ident -> transIdent ident



transAExp :: AExp -> Result
transAExp x = case x of
  EAdd aexp0 aexp -> transArith aexp0 "+" aexp
  ESub aexp0 aexp -> transArith aexp0 "-" aexp
  EMul aexp0 aexp -> transArith aexp0 "*" aexp
  EUmn aexp -> "-" ++ brArg transAExp aexp
  ECSetExp sexp -> "#" ++ brArg transSExp sexp
  EInt n    -> show n
  where
  transArith = transBinOp transAExp
